(0) Obligation:
JBC Problem based on JBC Program:
Manifest-Version: 1.0
Created-By: 1.6.0_16 (Sun Microsystems Inc.)
Main-Class: ListInt
/**
* A set of functions over lists of integers.
*
* All calls terminate.
*
* Julia + BinTerm prove that all calls terminate
*
* Note that cyclicity is introduced by the statement
* <tt>l1.tail.tail = l1</tt>. However, this is not enough to induce
* non-termination in the program. If you instead uncomment the line
* <tt>l0.tail.tail = l0</tt>, most of the calls cannot be proved to terminate
* anymore.
*
* @author <A HREF="mailto:fausto.spoto@univr.it">Fausto Spoto</A>
*/
public class ListInt {
private int head;
private ListInt tail;
public static void main(String[] args) {
ListInt l0 = new ListInt(5,new ListInt(6,null));
ListInt l1 = new ListInt(1,new ListInt(3,null));
l0.merge(l1);
l1.tail.tail = l1;
//l0.tail.tail = l0;
l0.append(l1);
l0.iter();
l0.reverseAcc(null);
l0.reverse();
}
public ListInt(int head, ListInt tail) {
this.head = head;
this.tail = tail;
}
private void iter() {
if (tail != null) tail.iter();
}
private ListInt append(ListInt other) {
if (tail == null) return new ListInt(head,other);
else return new ListInt(head,tail.append(other));
}
private ListInt reverseAcc(ListInt acc) {
if (tail == null) return new ListInt(head,acc);
else return tail.reverseAcc(new ListInt(head,acc));
}
private ListInt reverse() {
if (tail == null) return this;
else return tail.reverse().append(new ListInt(head,null));
}
private ListInt merge(ListInt other) {
if (other == null) return this;
else if (head <= other.head)
if (tail != null) return new ListInt(head,tail.merge(other));
else return new ListInt(head,other);
else return new ListInt(other.head,merge(other.tail));
}
}